package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class Toy2 {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("Toy2");
		 
         // Variables
         TypedData v2 = new TypedData("v2", Constants.TYPE_INTEGER);
         tiosts.addVariable(v2);
         
         // There are no parameters       
         
         // Input, output, and internal actions
         Action init = new Action("init2", Constants.ACTION_INTERNAL);
         tiosts.addAction(init);
         Action a = new Action("a", Constants.ACTION_INPUT);
         tiosts.addAction(a);
         
         // Locations
         Location start = new Location("Start2");
         tiosts.addLocation(start);
         Location s2 = new Location("S2");
         tiosts.addLocation(s2);
         Location s3 = new Location("S3");
         tiosts.addLocation(s3);        
         
         // Initial Condition
         tiosts.setInitialCondition("v2 > 0");
         
         // Initial Location
         tiosts.setInitialLocation(start);
         
         // Transitions
         tiosts.createTransition("Start2", "v2 > 0", Constants.GUARD_TRUE, init, null, null, "S2");
         tiosts.createTransition("S2", Constants.GUARD_TRUE, Constants.GUARD_TRUE, a, "v2 := 0", null, "S3");
         
         return tiosts;
		 
	 }

}

